Nuprl Lemma : ma-empty-feasible
0,22
postcript
pdf
Feasible()
latex
Definitions
,
Feasible(
M
)
,
,
mk-ma
,
ma-frame-compat(
A
;
B
)
,
x
dom(
f
).
v
=
f
(
x
)
P
(
x
;
v
)
,
x
dom(
f
)
,
b
,
State(
ds
)
,
<
a
,
b
>
,
nil
,
P
&
Q
,
x
:
A
.
B
(
x
)
,
P
Q
,
(
x
l
)
,
Id
,
False
,
x
:
A
B
(
x
)
,
Knd
,
t
T
,
IdLnk
Lemmas
IdLnk
wf
,
Knd
wf
,
false
wf
,
Id
wf
origin
x
dom(f). v=f(x) 
P(x;v) dom(f)
bx:A. B(x) Q l)
B(x) Txdom(f). v=f(x) P(x;v) dom(f)bx:A. B(x) Q l)B(x) T